\begin{tabbing}
$k$(v) sends [${\it tg}$,$f$(State(${\it ds}$), v)] on $l$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=sends $k$(v:$A$) on $l$:\+
\\[0ex]tagged([$\langle$${\it tg}$$,\,$$\lambda$$s$,$v$. [$f$($s$,$v$)]$\rangle$],State(${\it ds}$),v):${\it tg}$ : $T$
\-
\end{tabbing}